The behavior and operation of devices may be described using abstract state machines (ASMs). For each action that the device may take, the ASM defines conditions that must be met to effect changes to the state of the device. The conditions may be said to “guard” changes to the device state, and may thus be referred to as guards on the device state. For a more complete description of normalized ASMs, see Y. Gurevich, Evolving Algebra, 1993: Lipari Guide, and In E. Boerger, Specification and Validation Methods, pages 9-36, Oxford University Press, 1995. ASMs have applications beyond describing the behavior and operation of devices. For example, ASMs may describe the behavior and operation of software programs executing on a general purpose computer system.
Each unique combination of state settings, in other words, the values of all variables in the system, represents a state of the device in the ASM. For this reason, ASMs may have a large, even infinite number of states. Languages exist for specifying model programs (i.e., ASML, Spec#, etc.). The term model program refers to the embodiment of an ASM as a finite text written in a computer language. These languages often have supporting analysis tools that will reduce any specified model program into a finite state machine (FSM).
FIG. 1 is a prior art graphical representation of a finite state machine created from a specified model program. Well-known techniques exist for generating test suites from finite state machines (FSMs). FSMs define the behavior of a device in terms of device states and the events that result in state changes. However, due to the very large or infinite number of states of the ASM, it is often impractical to apply to ASMs the techniques used for generating test suites from ESMs. A previous patent application provides a manner of producing an FSM from an ASM (see “Generating a Test Suite from an Abstract State Machine,” U.S. Pat. No. 7,088,864, issued Aug. 8, 2006, which is incorporated herein by reference and is hereafter referred to as “GTSASM”), which leads to the application of FSM test suite generation techniques to ASMs. This prior application provides a way of generating test suites from an FSM generated from a model program.
During test case generation from a model program, a finite transition system is produced that encodes interesting or relevant runs of the model program (a process called “FSM generation”), and then the finite transition system is traversed to produce test cases. The finite transition system produced from a model program can also be used to verify the behavior (e.g., inputs, outputs, etc.) of an implementation under test (e.g., device, software, etc.). Although a model program is expressed as a finite text, it typically induces a transition system (an “unwinding” of the model program) with a very large or even infinite state space.